Model checking has been used to verify program behavior. For example, a tool takes a device driver program and builds a Boolean program and an associated model, and exhaustively tests the model according to certain properties (e.g., predicates) defined in a specification. If the predicates are not violated during state exploration of the model, then the driver is deemed verified for that specification. Verification involves testing the driver for all possible inputs. The analysis is conducted symbolically on the Boolean model of the driver, as opposed to the driver itself. A user provides a specification such as a set of predicates that they would like to be checked or verified on the program. A specification includes one or more predicates that verify certain properties. For example, if a driver acquires a lock on a resource, it should release the lock. However, exploration of the model is often impractical for many general purpose programs due to the complexity of an exploding state space.